package entities;


import java.util.HashSet; 



import entities.concept.Concept;
import entities.concept.NotConcept;
import entities.concept.OrConcept;
import entities.concept.PConcept;
import entities.vocabulary.Display;

public class Axiom {

	private Concept lhs;
	private Concept rhs;
	
	public Axiom(Concept lhs, Concept rhs){
		this.lhs = lhs;
		this.rhs = rhs;
	}
	
	//for a->b, get ~a or b. if a is top, just b, if a is bot, returns top.
	public Concept getConcept(){
		Concept ret = null;
		if(this.getLHS().isTop()){
			ret = this.getRHS();
		}else
		if(this.getLHS().isBot()){
			ret = entities.vocabulary.KBVocabulary.CONCEPT_TOP;
		}else{
			//return ~a or b
			HashSet<Concept> ors = new HashSet<Concept>();
			ors.add(this.getRHS());
			ors.add(new NotConcept(this.getLHS()));
			ret =  new OrConcept(ors);
		}
		return ret;
	}
	
	public Concept getLHS(){
		return this.lhs;
	}
	
	public Concept getRHS(){
		return this.rhs;
	}
	
	public boolean LHSPrimitive(){
		return (this.lhs instanceof PConcept);
	}
	
	public boolean LHSBinarySimple(){
		return this.lhs.isBinarySimple();
	}
	
	//transform this axiom into ("well-formed") disjunctive items, e.g. top => {A, B}
	public static HashSet<Concept> axiomToDisjuncts(InclusionAxiom axiom){
		HashSet<Concept> cons = new HashSet<Concept>();
		cons.add(axiom.getRHS());
		cons.add(new NotConcept(axiom.getLHS()));
		return Concept.reduceToDisjuncts(new OrConcept(cons));
	}
	
	public Axiom getPrimeCopy()  {
		if (this instanceof InclusionAxiom) {
			//TODO: hack! these shouldn't be null
			if (this.getLHS() != null && this.getRHS() != null ) {
				return new InclusionAxiom(this.getLHS().getPrimeCopy(), this.getRHS().getPrimeCopy());
			}
		}
		else if (this instanceof EquivalenceAxiom) {
			return new EquivalenceAxiom(this.getLHS().getPrimeCopy(), this.getRHS().getPrimeCopy());
		}
		//throw new Exception("Attempt to 'prime' Unrecognized Axiom Type.");
		return null;
	}
	
	@Override
	public String toString(){
		String ret = "";
		if(this instanceof InclusionAxiom){
			try{
			ret += this.getLHS() + " "+Display.IMPLIESUNICODE +" " + this.getRHS();
			}catch(Exception e){
				System.err.println(this.getLHS());
				e.printStackTrace();
				throw new RuntimeException();
			}
		}else if(this instanceof EquivalenceAxiom){
			ret += this.getLHS() + " "+ Display.EQAXIOMUNICODE + " "+ this.getRHS();
		}
		
		return ret;
	}

	
}
